es:ES, ff:FIFO, i:ff.C, e:{e:E| ff.R(i,e)} , j:{j:ff.C| ff.S(j,i,ff.Sender(i,e))} .
(i, j:ff.C, e:E. Dec(ff.S(i,j,e)))
 (ff.Decodes(i,e,(state when e))
 (=
 (ff.Codes(j,i,ff.Sender(i,e),(state when ff.Sender(i,e)))
 ( ff.T) 

latex

Definitions	False, P  Q, x(s), True, T, P  Q, t.1, A c B, x. t(x), P  Q, P & Q, x:A. B(x), , t  T, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ff.Codes, ff.Decodes, ff.T, ff.Sender, ff.S, ff.R, ff.C, x:A. B(x), A, P  Q, Dec(P), Q f P, Q  f P, for clients C sends FIFO   from j to i via (S[j,i],codes)   receives at i via (R[i],decodes), FIFO
Lemmas	true wf, squash wf, decidable wf, es-E wf, es-causle wf, es-state-when wf, antecedent-surjection wf, pi1 wf, event system wf, FIFO wf